Is it on the online notes by the way?

I'm still trying to get connections.

That was the mistake of doing it not in the 11th floor back here.

Okay but that means that if we find a mistake now we will still be able to correct it before

uploading this.

As usual with all our previous bloods we start with a bunch of derivations to do in sequence

system in question.

This is hopefully unproblematic.

We don't even use any sophisticated examples where you have some funny bunches on the left

hand side just to derivations between formulas.

In this case really it was just laziness so of course I have masking as stated here to

prove both the sequence, the left hand side sequence arrow right hand side and the right

hand side sequence arrow left hand side and similarly here.

And these are unproblematic hopefully.

Then we have a bit more fun and actually this connects already to what we were talking about

yesterday.

Today we have a rule which is, is this really double?

So this is one possible way of adding Boolean propositional base to BI.

So far the base BI that we had was intuitionistic but in fact two of the four classes of models

so here I mean it's not necessarily even TDRM, PDRM is enough, partial discrete resource

monoid and well this is a special formulation of excluded middle but one that is particularly

useful in derivations.

We are even thinking of adding some somewhat interesting one, not river one but in the

last minute we said that it's probably a bit too much fun if we don't give you too many

hints.

So we just ask you to prove that this rule is sound in the sense that we introduced yesterday.

So if you have under given valuation that the left hand side of this sequence is contained

in the right hand side and it's online, okay great.

If you have that the left hand side of this sequence is contained in the right hand side

of this sequence under given valuation in a discrete resource model and also left hand

side of this thing where of course this has to be in the five weeks proposition of collapse

blah blah blah is contained in the right hand side under the same valuation.

So there is a reason why we were so specific about discrete orders and in fact this really

extends an observation that we have already seen in the intuitionistic case that if you

have no meaningful order between things then you validate classical or just intuitionistic

logic.

It's just that here restricting to classical, restricting to discrete order doesn't mean

that you restrict to single points because you have some additional structure given of

course by the monoid business.

Then the next exercise which is intended to show problem with having bottom for completeness

results especially if you want to have completeness with respect to total rather than partial

resource monoid and semantically strange as this sequence looks like it is actually nowhere

as scary or nowhere as meaningless as it may seem on the first side.

This characterize this thing will be if you have bottom of the standard semantics, the

semantics that we introduced yesterday then if the relation, if the operation is totally

defined our monoid operation this will be always valid.

Again in the sense that we introduced yesterday for any valuation the left hand side will

be contained in the right hand side.

And this is another useful thing.

If you understand what is going on with this then it will be clear why having both this